b:. (b = tt)  (b) 

latex

ProofTree

Definitions	, t  T, P  Q, P  Q, P  Q, P  Q, x:A. B(x), True, if b then t else f fi , b, tt, Unit, , False, A, ff,
Lemmas	assert wf, btrue wf, bool wf, btrue neq bfalse, assert of ff